DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2016.23

Guarded Cubical Type Theory: Path Equality for Guarded Recursion

Authors: Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract

This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement GDTT with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. CTT is a variation of Martin-Löf type theory in which the identity type is replaced by abstract paths between terms. CTT provides a computational interpretation of functional extensionality, is conjectured to have decidable type checking, and has an implemented type checker. Our new type theory, called guarded cubical type theory, provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of CTT as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation, and present semantics in a presheaf category.

Cite as

Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{birkedal_et_al:LIPIcs.CSL.2016.23,
  author =	{Birkedal, Lars and Bizjak, Ale\v{s} and Clouston, Ranald and Grathwohl, Hans Bugge and Spitters, Bas and Vezzosi, Andrea},
  title =	{{Guarded Cubical Type Theory: Path Equality for Guarded Recursion}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.23},
  URN =		{urn:nbn:de:0030-drops-65638},
  doi =		{10.4230/LIPIcs.CSL.2016.23},
  annote =	{Keywords: Guarded Recursion, Dependent Type Theory, Cubical Type Theory, Denotational Semantics, Homotopy Type Theory}
}

Document

DOI: 10.4230/LIPIcs.CSL.2015.359

Functions out of Higher Truncations

Authors: Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract

In homotopy type theory, the truncation operator ||-||n (for a number n greater or equal to -1) is often useful if one does not care about the higher structure of a type and wants to avoid coherence problems. However, its elimination principle only allows to eliminate into n-types, which makes it hard to construct functions ||A||n -> B if B is not an n-type. This makes it desirable to derive more powerful elimination theorems. We show a first general result: If B is an (n+1)-type, then functions ||A||n -> B correspond exactly to functions A -> B that are constant on all (n+1)-st loop spaces. We give one "elementary" proof and one proof that uses a higher inductive type, both of which require some effort. As a sample application of our result, we show that we can construct "set-based" representations of 1-types, as long as they have "braided" loop spaces. The main result with one of its proofs and the application have been formalised in Agda.

Cite as

Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. Functions out of Higher Truncations. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 359-373, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{capriotti_et_al:LIPIcs.CSL.2015.359,
  author =	{Capriotti, Paolo and Kraus, Nicolai and Vezzosi, Andrea},
  title =	{{Functions out of Higher Truncations}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{359--373},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.359},
  URN =		{urn:nbn:de:0030-drops-54257},
  doi =		{10.4230/LIPIcs.CSL.2015.359},
  annote =	{Keywords: homotopy type theory, truncation elimination, constancy on loop spaces}
}

Search Results

Documents authored by Vezzosi, Andrea

Guarded Cubical Type Theory: Path Equality for Guarded Recursion

Abstract

Cite as

Functions out of Higher Truncations

Abstract

Cite as

Thanks for your feedback!

Could not send message